Cubical Type Theory
Cubical Type Theory
『Cubical Type Theory: a constructive interpretation of the univalence axiom』を読む
【1611.02108】 Cubical Type Theory: a constructive interpretation of the univalence axiom. 2016-11-07.
HoTTのUnivalence Axiom (UA)を計算可能にした理論らしい
Computational Type Theory
実装
Cubical Agda
確認用
Q. Cubical Type Theory
関連
Observational Type Theory
メモ
/mrsekut-p/Cubical Type Theory
【1611.02108】 Cubical Type Theory: a constructive interpretation of the univalence axiom. 2016-11-07.
cubical type theory in nLab
1Lab - 1Lab
Cubical Agda: a cold Introduction – Nextjournal
Type-Theoretic Truncation Levels - YouTube
https://www.youtube.com/watch?v=LWQqE2JcDSQ&list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9
>masahiro_sakaiCubical Type Theory は HoTT の univalence axiom をちゃんと計算できる形に解釈できる理論で、直観的にはパスをI=0,1からの関数として解釈する。実装としてはもともとcubicalttという実験的なプロトタイプ実装はあったけど、今回Agdaを拡張してfull-fledgedな実装を提案したという感じ。
Computational Type Theory 【1/5】 - Robert Harper - OPLSS 2018 - YouTube
https://www.youtube.com/watch?v=LE0SSLizYUI&list=PL0DsGHMPLUWXXA8RHzVZ2B5E5hP8CD15Z&index=1
調査用
Google.icon Cubical Type Theory(日)
Google.icon Cubical Type Theory(英)
Wikipedia.icon
Cubical Type Theory - Wikipedia(日)
Cubical Type Theory(検索) - Wikipedia(日)
Wikipedia.icon
Cubical Type Theory - Wikipedia(英)
Cubical Type Theory(検索) - Wikipedia(英)